Termination Proof Script

• Consider the SCC {13,17,19-22}. The usable rules are {1-3,6-12}. The constraints could not be solved.


• Consider the SCC {14}. The usable rules are {1-3,6-12}. By taking the AF π with π(first) = π(n__first) = π(SEL) = 1, π(cons) = 2 and π(from) = π(n__from) = [ ] together with the lexicographic path order with precedence 0 ≻ nil, activate ≻ from ≻ n__from and activate ≻ s ≻ n__s, the rules in {8,11} are weakly decreasing and the rules in {1-3,6,7,9,10,12,14} are strictly decreasing.